0 Prolog
↳1 PrologToPrologProblemTransformerProof (⇒, 86 ms)
↳2 Prolog
↳3 PrologToPiTRSProof (⇒, 0 ms)
↳4 PiTRS
↳5 DependencyPairsProof (⇔, 12 ms)
↳6 PiDP
↳7 DependencyGraphProof (⇔, 0 ms)
↳8 AND
↳9 PiDP
↳10 UsableRulesProof (⇔, 0 ms)
↳11 PiDP
↳12 PiDPToQDPProof (⇒, 11 ms)
↳13 QDP
↳14 QDPSizeChangeProof (⇔, 0 ms)
↳15 YES
↳16 PiDP
↳17 UsableRulesProof (⇔, 0 ms)
↳18 PiDP
↳19 PiDPToQDPProof (⇒, 0 ms)
↳20 QDP
↳21 MRRProof (⇔, 104 ms)
↳22 QDP
↳23 DependencyGraphProof (⇔, 0 ms)
↳24 TRUE
normalB_in_ga(op(op(T20, T21), T22), T7) → U2_ga(T20, T21, T22, T7, normalB_in_ga(op(T20, op(T21, T22)), T7))
normalB_in_ga(op(T39, op(T40, T41)), T7) → U3_ga(T39, T40, T41, T7, rewriteA_in_gga(T40, T41, X48))
rewriteA_in_gga(op(T67, T68), T69, op(T67, op(T68, T69))) → rewriteA_out_gga(op(T67, T68), T69, op(T67, op(T68, T69)))
rewriteA_in_gga(T76, op(T77, T78), op(T76, X90)) → U1_gga(T76, T77, T78, X90, rewriteA_in_gga(T77, T78, X90))
U1_gga(T76, T77, T78, X90, rewriteA_out_gga(T77, T78, X90)) → rewriteA_out_gga(T76, op(T77, T78), op(T76, X90))
U3_ga(T39, T40, T41, T7, rewriteA_out_gga(T40, T41, X48)) → normalB_out_ga(op(T39, op(T40, T41)), T7)
normalB_in_ga(op(T39, op(T40, T41)), T7) → U4_ga(T39, T40, T41, T7, rewriteA_in_gga(T40, T41, T48))
U4_ga(T39, T40, T41, T7, rewriteA_out_gga(T40, T41, T48)) → U5_ga(T39, T40, T41, T7, normalB_in_ga(op(T39, T48), T7))
normalB_in_ga(T90, T90) → normalB_out_ga(T90, T90)
U5_ga(T39, T40, T41, T7, normalB_out_ga(op(T39, T48), T7)) → normalB_out_ga(op(T39, op(T40, T41)), T7)
U2_ga(T20, T21, T22, T7, normalB_out_ga(op(T20, op(T21, T22)), T7)) → normalB_out_ga(op(op(T20, T21), T22), T7)
Infinitary Constructor Rewriting Termination of PiTRS implies Termination of Prolog
normalB_in_ga(op(op(T20, T21), T22), T7) → U2_ga(T20, T21, T22, T7, normalB_in_ga(op(T20, op(T21, T22)), T7))
normalB_in_ga(op(T39, op(T40, T41)), T7) → U3_ga(T39, T40, T41, T7, rewriteA_in_gga(T40, T41, X48))
rewriteA_in_gga(op(T67, T68), T69, op(T67, op(T68, T69))) → rewriteA_out_gga(op(T67, T68), T69, op(T67, op(T68, T69)))
rewriteA_in_gga(T76, op(T77, T78), op(T76, X90)) → U1_gga(T76, T77, T78, X90, rewriteA_in_gga(T77, T78, X90))
U1_gga(T76, T77, T78, X90, rewriteA_out_gga(T77, T78, X90)) → rewriteA_out_gga(T76, op(T77, T78), op(T76, X90))
U3_ga(T39, T40, T41, T7, rewriteA_out_gga(T40, T41, X48)) → normalB_out_ga(op(T39, op(T40, T41)), T7)
normalB_in_ga(op(T39, op(T40, T41)), T7) → U4_ga(T39, T40, T41, T7, rewriteA_in_gga(T40, T41, T48))
U4_ga(T39, T40, T41, T7, rewriteA_out_gga(T40, T41, T48)) → U5_ga(T39, T40, T41, T7, normalB_in_ga(op(T39, T48), T7))
normalB_in_ga(T90, T90) → normalB_out_ga(T90, T90)
U5_ga(T39, T40, T41, T7, normalB_out_ga(op(T39, T48), T7)) → normalB_out_ga(op(T39, op(T40, T41)), T7)
U2_ga(T20, T21, T22, T7, normalB_out_ga(op(T20, op(T21, T22)), T7)) → normalB_out_ga(op(op(T20, T21), T22), T7)
NORMALB_IN_GA(op(op(T20, T21), T22), T7) → U2_GA(T20, T21, T22, T7, normalB_in_ga(op(T20, op(T21, T22)), T7))
NORMALB_IN_GA(op(op(T20, T21), T22), T7) → NORMALB_IN_GA(op(T20, op(T21, T22)), T7)
NORMALB_IN_GA(op(T39, op(T40, T41)), T7) → U3_GA(T39, T40, T41, T7, rewriteA_in_gga(T40, T41, X48))
NORMALB_IN_GA(op(T39, op(T40, T41)), T7) → REWRITEA_IN_GGA(T40, T41, X48)
REWRITEA_IN_GGA(T76, op(T77, T78), op(T76, X90)) → U1_GGA(T76, T77, T78, X90, rewriteA_in_gga(T77, T78, X90))
REWRITEA_IN_GGA(T76, op(T77, T78), op(T76, X90)) → REWRITEA_IN_GGA(T77, T78, X90)
NORMALB_IN_GA(op(T39, op(T40, T41)), T7) → U4_GA(T39, T40, T41, T7, rewriteA_in_gga(T40, T41, T48))
U4_GA(T39, T40, T41, T7, rewriteA_out_gga(T40, T41, T48)) → U5_GA(T39, T40, T41, T7, normalB_in_ga(op(T39, T48), T7))
U4_GA(T39, T40, T41, T7, rewriteA_out_gga(T40, T41, T48)) → NORMALB_IN_GA(op(T39, T48), T7)
normalB_in_ga(op(op(T20, T21), T22), T7) → U2_ga(T20, T21, T22, T7, normalB_in_ga(op(T20, op(T21, T22)), T7))
normalB_in_ga(op(T39, op(T40, T41)), T7) → U3_ga(T39, T40, T41, T7, rewriteA_in_gga(T40, T41, X48))
rewriteA_in_gga(op(T67, T68), T69, op(T67, op(T68, T69))) → rewriteA_out_gga(op(T67, T68), T69, op(T67, op(T68, T69)))
rewriteA_in_gga(T76, op(T77, T78), op(T76, X90)) → U1_gga(T76, T77, T78, X90, rewriteA_in_gga(T77, T78, X90))
U1_gga(T76, T77, T78, X90, rewriteA_out_gga(T77, T78, X90)) → rewriteA_out_gga(T76, op(T77, T78), op(T76, X90))
U3_ga(T39, T40, T41, T7, rewriteA_out_gga(T40, T41, X48)) → normalB_out_ga(op(T39, op(T40, T41)), T7)
normalB_in_ga(op(T39, op(T40, T41)), T7) → U4_ga(T39, T40, T41, T7, rewriteA_in_gga(T40, T41, T48))
U4_ga(T39, T40, T41, T7, rewriteA_out_gga(T40, T41, T48)) → U5_ga(T39, T40, T41, T7, normalB_in_ga(op(T39, T48), T7))
normalB_in_ga(T90, T90) → normalB_out_ga(T90, T90)
U5_ga(T39, T40, T41, T7, normalB_out_ga(op(T39, T48), T7)) → normalB_out_ga(op(T39, op(T40, T41)), T7)
U2_ga(T20, T21, T22, T7, normalB_out_ga(op(T20, op(T21, T22)), T7)) → normalB_out_ga(op(op(T20, T21), T22), T7)
NORMALB_IN_GA(op(op(T20, T21), T22), T7) → U2_GA(T20, T21, T22, T7, normalB_in_ga(op(T20, op(T21, T22)), T7))
NORMALB_IN_GA(op(op(T20, T21), T22), T7) → NORMALB_IN_GA(op(T20, op(T21, T22)), T7)
NORMALB_IN_GA(op(T39, op(T40, T41)), T7) → U3_GA(T39, T40, T41, T7, rewriteA_in_gga(T40, T41, X48))
NORMALB_IN_GA(op(T39, op(T40, T41)), T7) → REWRITEA_IN_GGA(T40, T41, X48)
REWRITEA_IN_GGA(T76, op(T77, T78), op(T76, X90)) → U1_GGA(T76, T77, T78, X90, rewriteA_in_gga(T77, T78, X90))
REWRITEA_IN_GGA(T76, op(T77, T78), op(T76, X90)) → REWRITEA_IN_GGA(T77, T78, X90)
NORMALB_IN_GA(op(T39, op(T40, T41)), T7) → U4_GA(T39, T40, T41, T7, rewriteA_in_gga(T40, T41, T48))
U4_GA(T39, T40, T41, T7, rewriteA_out_gga(T40, T41, T48)) → U5_GA(T39, T40, T41, T7, normalB_in_ga(op(T39, T48), T7))
U4_GA(T39, T40, T41, T7, rewriteA_out_gga(T40, T41, T48)) → NORMALB_IN_GA(op(T39, T48), T7)
normalB_in_ga(op(op(T20, T21), T22), T7) → U2_ga(T20, T21, T22, T7, normalB_in_ga(op(T20, op(T21, T22)), T7))
normalB_in_ga(op(T39, op(T40, T41)), T7) → U3_ga(T39, T40, T41, T7, rewriteA_in_gga(T40, T41, X48))
rewriteA_in_gga(op(T67, T68), T69, op(T67, op(T68, T69))) → rewriteA_out_gga(op(T67, T68), T69, op(T67, op(T68, T69)))
rewriteA_in_gga(T76, op(T77, T78), op(T76, X90)) → U1_gga(T76, T77, T78, X90, rewriteA_in_gga(T77, T78, X90))
U1_gga(T76, T77, T78, X90, rewriteA_out_gga(T77, T78, X90)) → rewriteA_out_gga(T76, op(T77, T78), op(T76, X90))
U3_ga(T39, T40, T41, T7, rewriteA_out_gga(T40, T41, X48)) → normalB_out_ga(op(T39, op(T40, T41)), T7)
normalB_in_ga(op(T39, op(T40, T41)), T7) → U4_ga(T39, T40, T41, T7, rewriteA_in_gga(T40, T41, T48))
U4_ga(T39, T40, T41, T7, rewriteA_out_gga(T40, T41, T48)) → U5_ga(T39, T40, T41, T7, normalB_in_ga(op(T39, T48), T7))
normalB_in_ga(T90, T90) → normalB_out_ga(T90, T90)
U5_ga(T39, T40, T41, T7, normalB_out_ga(op(T39, T48), T7)) → normalB_out_ga(op(T39, op(T40, T41)), T7)
U2_ga(T20, T21, T22, T7, normalB_out_ga(op(T20, op(T21, T22)), T7)) → normalB_out_ga(op(op(T20, T21), T22), T7)
REWRITEA_IN_GGA(T76, op(T77, T78), op(T76, X90)) → REWRITEA_IN_GGA(T77, T78, X90)
normalB_in_ga(op(op(T20, T21), T22), T7) → U2_ga(T20, T21, T22, T7, normalB_in_ga(op(T20, op(T21, T22)), T7))
normalB_in_ga(op(T39, op(T40, T41)), T7) → U3_ga(T39, T40, T41, T7, rewriteA_in_gga(T40, T41, X48))
rewriteA_in_gga(op(T67, T68), T69, op(T67, op(T68, T69))) → rewriteA_out_gga(op(T67, T68), T69, op(T67, op(T68, T69)))
rewriteA_in_gga(T76, op(T77, T78), op(T76, X90)) → U1_gga(T76, T77, T78, X90, rewriteA_in_gga(T77, T78, X90))
U1_gga(T76, T77, T78, X90, rewriteA_out_gga(T77, T78, X90)) → rewriteA_out_gga(T76, op(T77, T78), op(T76, X90))
U3_ga(T39, T40, T41, T7, rewriteA_out_gga(T40, T41, X48)) → normalB_out_ga(op(T39, op(T40, T41)), T7)
normalB_in_ga(op(T39, op(T40, T41)), T7) → U4_ga(T39, T40, T41, T7, rewriteA_in_gga(T40, T41, T48))
U4_ga(T39, T40, T41, T7, rewriteA_out_gga(T40, T41, T48)) → U5_ga(T39, T40, T41, T7, normalB_in_ga(op(T39, T48), T7))
normalB_in_ga(T90, T90) → normalB_out_ga(T90, T90)
U5_ga(T39, T40, T41, T7, normalB_out_ga(op(T39, T48), T7)) → normalB_out_ga(op(T39, op(T40, T41)), T7)
U2_ga(T20, T21, T22, T7, normalB_out_ga(op(T20, op(T21, T22)), T7)) → normalB_out_ga(op(op(T20, T21), T22), T7)
REWRITEA_IN_GGA(T76, op(T77, T78), op(T76, X90)) → REWRITEA_IN_GGA(T77, T78, X90)
REWRITEA_IN_GGA(T76, op(T77, T78)) → REWRITEA_IN_GGA(T77, T78)
From the DPs we obtained the following set of size-change graphs:
NORMALB_IN_GA(op(T39, op(T40, T41)), T7) → U4_GA(T39, T40, T41, T7, rewriteA_in_gga(T40, T41, T48))
U4_GA(T39, T40, T41, T7, rewriteA_out_gga(T40, T41, T48)) → NORMALB_IN_GA(op(T39, T48), T7)
NORMALB_IN_GA(op(op(T20, T21), T22), T7) → NORMALB_IN_GA(op(T20, op(T21, T22)), T7)
normalB_in_ga(op(op(T20, T21), T22), T7) → U2_ga(T20, T21, T22, T7, normalB_in_ga(op(T20, op(T21, T22)), T7))
normalB_in_ga(op(T39, op(T40, T41)), T7) → U3_ga(T39, T40, T41, T7, rewriteA_in_gga(T40, T41, X48))
rewriteA_in_gga(op(T67, T68), T69, op(T67, op(T68, T69))) → rewriteA_out_gga(op(T67, T68), T69, op(T67, op(T68, T69)))
rewriteA_in_gga(T76, op(T77, T78), op(T76, X90)) → U1_gga(T76, T77, T78, X90, rewriteA_in_gga(T77, T78, X90))
U1_gga(T76, T77, T78, X90, rewriteA_out_gga(T77, T78, X90)) → rewriteA_out_gga(T76, op(T77, T78), op(T76, X90))
U3_ga(T39, T40, T41, T7, rewriteA_out_gga(T40, T41, X48)) → normalB_out_ga(op(T39, op(T40, T41)), T7)
normalB_in_ga(op(T39, op(T40, T41)), T7) → U4_ga(T39, T40, T41, T7, rewriteA_in_gga(T40, T41, T48))
U4_ga(T39, T40, T41, T7, rewriteA_out_gga(T40, T41, T48)) → U5_ga(T39, T40, T41, T7, normalB_in_ga(op(T39, T48), T7))
normalB_in_ga(T90, T90) → normalB_out_ga(T90, T90)
U5_ga(T39, T40, T41, T7, normalB_out_ga(op(T39, T48), T7)) → normalB_out_ga(op(T39, op(T40, T41)), T7)
U2_ga(T20, T21, T22, T7, normalB_out_ga(op(T20, op(T21, T22)), T7)) → normalB_out_ga(op(op(T20, T21), T22), T7)
NORMALB_IN_GA(op(T39, op(T40, T41)), T7) → U4_GA(T39, T40, T41, T7, rewriteA_in_gga(T40, T41, T48))
U4_GA(T39, T40, T41, T7, rewriteA_out_gga(T40, T41, T48)) → NORMALB_IN_GA(op(T39, T48), T7)
NORMALB_IN_GA(op(op(T20, T21), T22), T7) → NORMALB_IN_GA(op(T20, op(T21, T22)), T7)
rewriteA_in_gga(op(T67, T68), T69, op(T67, op(T68, T69))) → rewriteA_out_gga(op(T67, T68), T69, op(T67, op(T68, T69)))
rewriteA_in_gga(T76, op(T77, T78), op(T76, X90)) → U1_gga(T76, T77, T78, X90, rewriteA_in_gga(T77, T78, X90))
U1_gga(T76, T77, T78, X90, rewriteA_out_gga(T77, T78, X90)) → rewriteA_out_gga(T76, op(T77, T78), op(T76, X90))
NORMALB_IN_GA(op(T39, op(T40, T41))) → U4_GA(T39, rewriteA_in_gga(T40, T41))
U4_GA(T39, rewriteA_out_gga(T48)) → NORMALB_IN_GA(op(T39, T48))
NORMALB_IN_GA(op(op(T20, T21), T22)) → NORMALB_IN_GA(op(T20, op(T21, T22)))
rewriteA_in_gga(op(T67, T68), T69) → rewriteA_out_gga(op(T67, op(T68, T69)))
rewriteA_in_gga(T76, op(T77, T78)) → U1_gga(T76, rewriteA_in_gga(T77, T78))
U1_gga(T76, rewriteA_out_gga(X90)) → rewriteA_out_gga(op(T76, X90))
rewriteA_in_gga(x0, x1)
U1_gga(x0, x1)
NORMALB_IN_GA(op(T39, op(T40, T41))) → U4_GA(T39, rewriteA_in_gga(T40, T41))
NORMALB_IN_GA(op(op(T20, T21), T22)) → NORMALB_IN_GA(op(T20, op(T21, T22)))
POL(NORMALB_IN_GA(x1)) = x1
POL(U1_gga(x1, x2)) = 2 + 2·x1 + x2
POL(U4_GA(x1, x2)) = 2 + 2·x1 + x2
POL(op(x1, x2)) = 2 + 2·x1 + x2
POL(rewriteA_in_gga(x1, x2)) = 2·x1 + x2
POL(rewriteA_out_gga(x1)) = x1
U4_GA(T39, rewriteA_out_gga(T48)) → NORMALB_IN_GA(op(T39, T48))
rewriteA_in_gga(op(T67, T68), T69) → rewriteA_out_gga(op(T67, op(T68, T69)))
rewriteA_in_gga(T76, op(T77, T78)) → U1_gga(T76, rewriteA_in_gga(T77, T78))
U1_gga(T76, rewriteA_out_gga(X90)) → rewriteA_out_gga(op(T76, X90))
rewriteA_in_gga(x0, x1)
U1_gga(x0, x1)